(set-info :source |fuzzsmt|)
(set-info :smt-lib-version 2.0)
(set-info :category "random")
(set-info :status unknown)
(set-logic QF_UF)
(declare-sort S0 0)
(declare-sort S1 0)
(declare-sort S2 0)
(declare-fun v0 () S0)
(declare-fun v1 () S1)
(declare-fun v2 () S2)
(declare-fun f0 ( S1 S1 S2) S1)
(declare-fun f1 ( S2 S1) S2)
(declare-fun f2 ( S2 S2) S1)
(declare-fun f3 ( S1) S1)
(declare-fun f4 ( S0 S1) S1)
(declare-fun f5 ( S2 S0) S1)
(declare-fun f6 ( S0) S0)
(declare-fun p0 ( S1 S2) Bool)
(declare-fun p1 ( S2) Bool)
(declare-fun p2 ( S1 S0 S2) Bool)
(declare-fun p3 ( S1 S0) Bool)
(declare-fun p4 ( S2 S1) Bool)
(assert (let ((e3 (f3 v1)))
(let ((e4 (f6 v0)))
(let ((e5 (f2 v2 v2)))
(let ((e6 (f2 v2 v2)))
(let ((e7 (f6 v0)))
(let ((e8 (f1 v2 e5)))
(let ((e9 (f0 e3 e5 e8)))
(let ((e10 (f6 v0)))
(let ((e11 (f6 e10)))
(let ((e12 (f6 v0)))
(let ((e13 (f1 v2 e5)))
(let ((e14 (f4 e11 e5)))
(let ((e15 (f0 e9 e14 v2)))
(let ((e16 (f0 e5 v1 v2)))
(let ((e17 (f5 e8 e7)))
(let ((e18 (p4 v2 e6)))
(let ((e19 (p4 e8 e9)))
(let ((e20 (p1 e13)))
(let ((e21 (distinct e7 e4)))
(let ((e22 (p1 e13)))
(let ((e23 (p1 e13)))
(let ((e24 (p1 e8)))
(let ((e25 (= e16 v1)))
(let ((e26 (p1 e8)))
(let ((e27 (p2 v1 e7 e8)))
(let ((e28 (p3 e3 e4)))
(let ((e29 (= e11 e12)))
(let ((e30 (p3 e5 e7)))
(let ((e31 (p3 e14 e11)))
(let ((e32 (p4 e8 e17)))
(let ((e33 (distinct e10 e12)))
(let ((e34 (distinct v0 e10)))
(let ((e35 (= e15 v1)))
(let ((e36 (p0 e3 e13)))
(let ((e37 (ite e29 e5 e6)))
(let ((e38 (ite e20 e17 e16)))
(let ((e39 (ite e27 v2 e13)))
(let ((e40 (ite e35 e11 v0)))
(let ((e41 (ite e36 e9 e37)))
(let ((e42 (ite e33 e13 e13)))
(let ((e43 (ite e33 e7 e11)))
(let ((e44 (ite e31 e8 e42)))
(let ((e45 (ite e24 e44 e13)))
(let ((e46 (ite e19 e15 e6)))
(let ((e47 (ite e31 e10 e11)))
(let ((e48 (ite e25 e4 v0)))
(let ((e49 (ite e34 e12 e12)))
(let ((e50 (ite e22 e14 e3)))
(let ((e51 (ite e23 v1 e37)))
(let ((e52 (ite e25 e13 v2)))
(let ((e53 (ite e24 e40 e11)))
(let ((e54 (ite e18 e47 e40)))
(let ((e55 (ite e28 e13 e45)))
(let ((e56 (ite e21 e15 e37)))
(let ((e57 (ite e35 e4 e10)))
(let ((e58 (ite e18 e15 e46)))
(let ((e59 (ite e36 e53 e43)))
(let ((e60 (ite e32 e11 e53)))
(let ((e61 (ite e34 e41 e14)))
(let ((e62 (ite e21 e7 v0)))
(let ((e63 (ite e26 e41 e3)))
(let ((e64 (ite e30 e38 e38)))
(let ((e65 (p0 e6 v2)))
(let ((e66 (distinct e56 e17)))
(let ((e67 (p3 v1 e62)))
(let ((e68 (= e8 e8)))
(let ((e69 (distinct e49 e11)))
(let ((e70 (distinct e54 e60)))
(let ((e71 (p0 e17 e42)))
(let ((e72 (p2 e61 e7 e13)))
(let ((e73 (distinct e15 e5)))
(let ((e74 (p1 e39)))
(let ((e75 (p4 e55 e6)))
(let ((e76 (distinct e43 e54)))
(let ((e77 (p0 e56 e55)))
(let ((e78 (= e4 e7)))
(let ((e79 (p4 e45 e17)))
(let ((e80 (distinct e41 e50)))
(let ((e81 (p3 v1 e60)))
(let ((e82 (= v0 e60)))
(let ((e83 (p2 e61 v0 e42)))
(let ((e84 (p4 e44 e5)))
(let ((e85 (= e63 e41)))
(let ((e86 (p1 e42)))
(let ((e87 (p4 e44 e46)))
(let ((e88 (= e64 e15)))
(let ((e89 (p1 e52)))
(let ((e90 (= e16 e51)))
(let ((e91 (= e59 e54)))
(let ((e92 (p2 e15 e43 e45)))
(let ((e93 (p2 e3 e43 e52)))
(let ((e94 (p3 e6 e49)))
(let ((e95 (distinct e57 e62)))
(let ((e96 (p3 e9 e40)))
(let ((e97 (p1 v2)))
(let ((e98 (distinct e47 e12)))
(let ((e99 (= e53 e59)))
(let ((e100 (= e10 e10)))
(let ((e101 (p1 e45)))
(let ((e102 (distinct e58 e58)))
(let ((e103 (p4 e45 e14)))
(let ((e104 (p1 e13)))
(let ((e105 (distinct e38 e58)))
(let ((e106 (distinct e48 e11)))
(let ((e107 (= e37 e16)))
(let ((e108 (and e95 e73)))
(let ((e109 (or e91 e99)))
(let ((e110 (xor e28 e33)))
(let ((e111 (not e75)))
(let ((e112 (ite e72 e29 e29)))
(let ((e113 (not e74)))
(let ((e114 (ite e26 e104 e25)))
(let ((e115 (xor e102 e89)))
(let ((e116 (= e112 e19)))
(let ((e117 (xor e23 e115)))
(let ((e118 (and e21 e82)))
(let ((e119 (=> e80 e85)))
(let ((e120 (not e96)))
(let ((e121 (xor e68 e114)))
(let ((e122 (=> e98 e35)))
(let ((e123 (and e84 e106)))
(let ((e124 (= e78 e76)))
(let ((e125 (xor e111 e31)))
(let ((e126 (not e87)))
(let ((e127 (ite e108 e108 e94)))
(let ((e128 (xor e113 e77)))
(let ((e129 (not e88)))
(let ((e130 (and e129 e116)))
(let ((e131 (ite e65 e107 e110)))
(let ((e132 (= e27 e69)))
(let ((e133 (or e117 e34)))
(let ((e134 (= e30 e20)))
(let ((e135 (not e100)))
(let ((e136 (= e66 e93)))
(let ((e137 (or e127 e83)))
(let ((e138 (or e134 e136)))
(let ((e139 (= e130 e86)))
(let ((e140 (and e36 e22)))
(let ((e141 (xor e79 e67)))
(let ((e142 (not e90)))
(let ((e143 (or e141 e103)))
(let ((e144 (=> e124 e122)))
(let ((e145 (= e135 e97)))
(let ((e146 (xor e145 e131)))
(let ((e147 (not e139)))
(let ((e148 (not e121)))
(let ((e149 (xor e147 e18)))
(let ((e150 (not e146)))
(let ((e151 (not e133)))
(let ((e152 (=> e119 e24)))
(let ((e153 (or e71 e125)))
(let ((e154 (= e109 e151)))
(let ((e155 (not e132)))
(let ((e156 (= e150 e92)))
(let ((e157 (=> e156 e149)))
(let ((e158 (= e126 e137)))
(let ((e159 (=> e154 e32)))
(let ((e160 (xor e152 e120)))
(let ((e161 (and e160 e158)))
(let ((e162 (= e153 e105)))
(let ((e163 (and e144 e155)))
(let ((e164 (not e70)))
(let ((e165 (or e138 e164)))
(let ((e166 (xor e161 e143)))
(let ((e167 (or e123 e163)))
(let ((e168 (not e142)))
(let ((e169 (ite e118 e128 e118)))
(let ((e170 (xor e159 e159)))
(let ((e171 (xor e165 e170)))
(let ((e172 (= e171 e81)))
(let ((e173 (not e169)))
(let ((e174 (xor e173 e148)))
(let ((e175 (= e167 e167)))
(let ((e176 (= e140 e140)))
(let ((e177 (not e166)))
(let ((e178 (ite e172 e162 e168)))
(let ((e179 (or e101 e174)))
(let ((e180 (=> e178 e175)))
(let ((e181 (not e179)))
(let ((e182 (or e177 e176)))
(let ((e183 (xor e180 e157)))
(let ((e184 (not e183)))
(let ((e185 (=> e184 e182)))
(let ((e186 (and e185 e185)))
(let ((e187 (=> e186 e181)))
e187
))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))

(check-sat)
